(set-option :model_validate true)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v8 Bool)
(declare-const r0 Real)
(declare-const r2 Real)
(declare-const r5 Real)
(declare-const v10 Bool)
(push 1)
(assert (and v2 v0 v5 (> (tanh r2) r0 (tanh r2)) v10))
(check-sat)
(declare-sort S0 0)
(declare-const v12 Bool)
(assert (xor (and (or v1 v2 v5) (<= 0.05 0.5685) v2 v2 (> (tanh r2) r0 (tanh r2))) v1 v12 v10 (= (or v1 v2 v5) v8 v5 v0) (<= 761905677.0 r5) (and (or v1 v2 v5) (<= 0.05 0.5685) v2 v2 (> (tanh r2) r0 (tanh r2))) v0))
(pop 1)
(declare-const v13 Bool)
(assert (xor v3 v13 (> (tanh r2) r0 (tanh r2)) (> (tanh r2) r0 (tanh r2)) (> (tanh r2) r0 (tanh r2)) (> (tanh r2) r0 (tanh r2)) v2))
(check-sat)
(reset)
(exit)

(set-option :proof true)
(set-option :model_validate true)
(set-option :smt.random_seed 1)
(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(assert (or (= c 1) (= (/ 1 a) 0)))
(assert (= b 1))
(assert (not (= a (- 1))))
(check-sat)
(check-sat)
(reset)
(set-option :smt.phase_selection 5)
(set-option :proof true)
(set-option :model_validate true)
(declare-fun a () Real)
(assert (> (/ 2 a) (/ 1 a) 0))
(check-sat)
(check-sat)
(get-model)